$\forall$${\it es}$:ES, $T$, $C$:Type, ${\it Out}$:AbsInterface(:$C$ $\times$ $T$). abs{-}R $\in$ $C$$\rightarrow$E$\rightarrow\mathbb{P}$